package simplytypedinference

/**
   * Slightly adapted from parser for untyped lambda calculus by Miles Sabin 
   */

trait LTerm {
  def toString_(ctx: Context[NameBinding]) : String = toString
}


 case class Tru extends LTerm {
    override def toString_(ctx: Context[NameBinding]) = "true"
 }
 case class Fls extends LTerm {
   override def toString_(ctx: Context[NameBinding]) = "false"
 }
 case class If(cond: LTerm, pos: LTerm, neg: LTerm) extends LTerm {
   override def toString_(ctx: Context[NameBinding]) = {
     "if "+cond.toString_(ctx)+" then "+pos.toString_(ctx)+" else "+neg.toString_(ctx)
   }
 }


 case class V(n: Int) extends LTerm {
   override def toString_(ctx: Context[NameBinding]) = ctx(n).name
 }
 case class L(x: String, ty: LType, t:LTerm) extends LTerm {
   override def toString_(ctx: Context[NameBinding]) = {
     val (ctx2, x2) = NameContext.pickDisplayName(x,ctx)
     "(\\"+x2+":"+ty+" ."+t.toString_(ctx2)+")"
   }
 }
 case class A(t1:LTerm, t2:LTerm) extends LTerm {
   override def toString_(ctx: Context[NameBinding]) = 
     "("+t1.toString_(ctx) + " " + t2.toString_(ctx) + ")"
 }
 
 case class Let(n: Name, t1: LTerm, t2: LTerm) extends LTerm {
   override def toString_(ctx:Context[NameBinding]) = {
     val (ctx2, x2) = NameContext.pickDisplayName(n.n,ctx)
     "let "+x2+" = " +t1.toString_(ctx) + " in " +(t2).toString_(ctx2)
   }
   override def toString = "let "+n+" = "+t1+" in "+t2
 }
 

 
 
 
 case class Unit extends LTerm {
   override def toString = "unit"
 }
 
 case class Lit(n: int) extends LTerm {
   override def toString = n.toString
 }
 
 
 case class Name(n: String) extends LTerm {
   override def toString = n
 }
 case class Ref(n: Name) extends LTerm {
   def value = n
 }
  
 case class Lam(n: Name,ty: LType, t: LTerm) extends LTerm
 {
   override def toString = "(\\ "+n+":"+ty+" -> "+t+")"
 } 
  
 case class App(t1: LTerm, t2: LTerm) extends LTerm
 {
   override def toString = "("+t1+" "+t2+")"
 } 
 
 case class Sequ(t1: LTerm, t2: LTerm) extends LTerm
 {
   override def toString = t1 +"; "+ t2     
 }
  

  

  

  
  /*
    
  trait PrimLTerm extends LTerm
  {
    def apply(n: Lit) : LTerm
  }

  case class PrimPlus extends PrimLTerm
  {
    def apply(x: Lit) = new PrimLTerm{ def apply(y: Lit) = Lit(x.n+y.n) }
  }

  case class PrimMinus extends PrimLTerm
  {
    def apply(x: Lit) = new PrimLTerm{ def apply(y: Lit) = Lit(x.n-y.n) }
  }
  
  case class PrimMultiply extends PrimLTerm
  {
    def apply(x: Lit) = new PrimLTerm{ def apply(y: Lit) = Lit(x.n*y.n) }
  }

  case class PrimDivide extends PrimLTerm
  {
    def apply(x: Lit) = new PrimLTerm{ def apply(y: Lit) = Lit(x.n/y.n) }
  }

  case class PrimEquals extends PrimLTerm
  {
    def apply(x: Lit) = new PrimLTerm{ def apply(y: Lit) =  if (x.n == y.n) Tru else Fls}
  }
*/